\begin{tabbing}
interleaved\_family\_occurence($T$;$I$;$L$;$L_{2}$;$f$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$i$:$I$. increasing($f$($i$);$\parallel$$L$($i$)$\parallel$) \& ($\forall$$j$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$($i$)$\parallel$}}$. ($L$($i$))[$j$] $=$ $L_{2}$[$f$($i$,$j$)]))\+
\\[0ex]\& ($\forall$$i_{1}$, $i_{2}$:$I$. $\neg$$i_{1}$ $=$ $i_{2}$ $\Rightarrow$ ($\forall$$j_{1}$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$($i_{1}$)$\parallel$}}$, $j_{2}$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$($i_{2}$)$\parallel$}}$. $\neg$$f$($i_{1}$,$j_{1}$) $=$ $f$($i_{2}$,$j_{2}$)))
\\[0ex]\& ($\forall$$x$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L_{2}$$\parallel$}}$. $\exists$$i$:$I$, $j$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$($i$)$\parallel$}}$. $x$ $=$ $f$($i$,$j$))
\-
\end{tabbing}